Nuprl Lemma : es-frame_wf
11,40
postcript
pdf
es
:ES,
i
:Id,
L
:(Knd List),
x
:Id,
T
:Type. @
i
only
L
affect
x
:
T
latex
Definitions
P
&
Q
,
@
i
(
x
:
T
)
,
t
.1
,
E
,
s
=
t
,
P
Q
,
A
,
t
T
,
{
T
}
,
x
:
A
.
B
(
x
)
,
SQType(
T
)
,
Id
,
,
s
~
t
,
Atom$n
,
vartype(
i
;
x
)
,
x
when
e
,
(
x
after
e
)
,
{
x
:
A
|
B
(
x
)}
,
ES
,
Knd
,
type
List
,
Type
,
x
:
A
B
(
x
)
,
loc(
e
)
,
kind(
e
)
,
(
x
l
)
,
x
.
t
(
x
)
,
e
@
i
.
P
(
e
)
,
A
c
B
,
@
i
only
L
affect
x
:
T
Lemmas
es-dtype
wf
,
alle-at
wf
,
not
wf
,
l
member
wf
,
es-kind
wf
,
es-E
wf
,
es-loc
wf
,
Knd
wf
,
event
system
wf
,
es-after
wf
,
es-when
wf
,
Id
wf
,
Id
sq
origin
es:ES, i:Id, L:(Knd List), x:Id, T:Type. @i only L affect x:T 
es:ES, i:Id, L:(Knd List), x:Id, T:Type. @i only L affect x:T 
Q
A Tx:A. B(x)
B(x) l)
x. t(x)e@i. P(e)
B